Theorem 3impia 1119

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)

Hypothesis

Ref	Expression
3impia.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Assertion

Ref	Expression
3impia	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impia

Step	Hyp	Ref	Expression
1		3impia.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	expimpd 457	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	3impib 1118	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1091

This theorem is referenced by:  mopick2  2638  3gencl  3439  vtoclgft  3458  mob2  3617  moi  3620  reupick3  4220  disjne  4355  elpr2elpr  4765  disji2  5021  disji  5022  tz7.2  5520  sofld  6030  ordintdif  6240  funopg  6392  fvun1  6780  fvopab6  6829  fveqressseq  6878  fvcofneq  6890  fprg  6948  2f1fvneq  7050  isores3  7122  ovmpt4g  7334  ovmpos  7335  ov2gf  7336  ofrval  7458  sorpssuni  7498  sorpssint  7499  poxp  7873  suppss2  7920  frrlem12  8016  smoel  8075  smoord  8080  smogt  8082  oaass  8267  oewordi  8297  oeoalem  8302  oeoelem  8304  nnawordi  8327  nnaass  8328  qsel  8456  xpdom3  8721  onsdominel  8773  mapdom3  8796  fisseneq  8865  cantnflem1  9282  cfslbn  9846  cfsmolem  9849  cfcoflem  9851  infpssrlem4  9885  fin23lem7  9895  fin23lem25  9903  isf34lem7  9958  hsmexlem2  10006  axcc3  10017  axdc4lem  10034  tskss  10337  gruss  10375  gruurn  10377  gruiun  10378  gruel  10382  gruen  10391  grudomon  10396  grothac  10409  axpre-sup  10748  axsup  10873  addn0nid  11217  letrp1  11641  p1le  11642  lemul1a  11651  infrelb  11782  zextle  12215  zextlt  12216  btwnnz  12218  gtndiv  12219  uzind2  12235  fzind  12240  eluzsub  12435  zsupss  12498  xrltne  12718  lemaxle  12750  qbtwnre  12754  qbtwnxr  12755  xlemul1a  12843  icogelb  12951  iccleub  12955  iccsplit  13038  uzsubsubfz  13099  elfz0fzfz0  13182  difelfznle  13191  fvffz0  13195  elfzo0le  13251  fzonmapblen  13253  fzofzim  13254  ceile  13387  modadd1  13446  muladdmodid  13449  modmul1  13462  modirr  13480  fsuppmapnn0fiub0  13531  expcl2lem  13612  expclzlem  13624  expnegz  13634  leexp2r  13709  bcval4  13838  bccmpl  13840  hashbnd  13867  hashunsnggt  13926  hashgt23el  13956  elovmpowrd  14078  ccatval2  14100  ccatrcl1  14116  wrdl1s1  14136  ccat2s1fvw  14166  ccat2s1fvwOLD  14167  swrdsb0eq  14193  swrdccatin1  14255  pfxccatpfx2  14267  repswswrd  14314  cshwcsh2id  14358  absexpz  14834  climbdd  15200  iseraltlem2  15211  binomfallfac  15566  dvdsle  15834  divalgb  15928  ndvdssub  15933  dvdsgcd  16067  dfgcd2  16069  rplpwr  16082  lcmgcdlem  16126  lcmfunsn  16164  coprmdvds1  16172  qredeq  16177  2mulprm  16213  prmdvdsexpr  16237  nnnn0modprm0  16322  prm23ge5  16331  pcexp  16375  difsqpwdvds  16403  prmpwdvds  16420  ramcl  16545  cshwshashlem3  16614  cshwrepswhash1  16619  elrestr  16887  mreintcl  17052  mremre  17061  mrieqv2d  17096  initoeu2lem1  17474  funcestrcsetclem9  17609  funcsetcestrclem9  17624  prstr  17761  drsdirfi  17766  latnlej  17916  latnlej2  17919  acsdrsel  18003  acsdrscl  18006  mrelatglb  18020  mrelatlub  18022  isnmgm  18072  grpasscan1  18380  grpinvnz  18388  mulgneg2  18479  gsmsymgrfix  18774  f1omvdco2  18794  symggen  18816  odcl2  18910  odhash3  18919  lsmss1  19009  lsmss2  19011  efgred  19092  efgcpbl  19100  ablfacrp  19407  ablfac1eu  19414  ablfaclem3  19428  dvdsrmul1  19625  dvdsunit  19635  irredmul  19681  lmodlema  19858  psgnodpmr  20506  phlssphl  20575  lindsss  20740  lindfmm  20743  ply1scln0  21166  dmatelnd  21347  mdetdiaglem  21449  mdet0  21457  mdetunilem7  21469  slesolinv  21531  cramerimplem3  21536  cpmatpmat  21561  m2cpminvid2lem  21605  chfacfscmul0  21709  chfacfpmmul0  21713  riinopn  21759  clsndisj  21926  cnpf2  22101  hausnei2  22204  cmpcov  22240  cmpfii  22260  unconn  22280  t1connperf  22287  nrmr0reg  22600  fbfinnfr  22692  filuni  22736  alexsubALT  22902  tmdgsum  22946  cuspcvg  23152  mopni  23344  isngp4  23464  metdsre  23704  iimulcl  23788  phtpc01  23847  clmmulg  23952  cfilucfil4  24172  bcthlem5  24179  bcth  24180  bcth3  24182  itg1le  24565  itg2le  24591  bddmulibl  24690  bddiblnc  24693  dvnres  24782  cpnord  24786  dvnfre  24803  deg1ge  24950  dgr1term  25108  aaliou3lem2  25190  sincosq1lem  25341  cxpge0  25525  cxpmul2  25531  logrec  25600  logbgcd1irr  25631  sqfpc  25973  bcmono  26112  gausslemma2dlem1a  26200  gausslemma2dlem2  26202  gausslemma2dlem4  26204  2lgsoddprmlem3  26249  pntrmax  26399  qabvexp  26461  ostth2lem2  26469  ax5seglem4  26977  axeuclidlem  27007  uhgredgrnv  27175  usgredg4  27259  nbuhgr2vtx1edgblem  27393  vtxduhgr0e  27520  vtxduhgr0nedg  27534  rusgrpropnb  27625  uspgr2wlkeqi  27689  redwlklem  27713  lfgrwlkprop  27729  2pthnloop  27772  spthonepeq  27793  pthdlem2lem  27808  crctcshwlkn0lem3  27850  crctcshwlkn0lem5  27852  crctcshwlkn0lem7  27854  crctcshwlkn0  27859  wlkiswwlks1  27905  wlkiswwlks2  27913  wlkiswwlksupgr2  27915  wwlksnext  27931  wwlksnextproplem2  27948  wspthsnonn0vne  27955  2pthon3v  27981  rusgrnumwwlk  28013  erclwwlkeqlen  28056  erclwwlksym  28058  erclwwlktr  28059  erclwwlkneqlen  28105  erclwwlknsym  28107  erclwwlkntr  28108  uhgr3cyclex  28219  upgreupthseg  28246  eupth2lem3lem4  28268  eucrctshift  28280  4cycl2vnunb  28327  nvs  28698  nvtri  28705  nmlno0  28830  nmlnoubi  28831  ubth  28908  hlipgt0  28949  ocnel  29333  elspansn2  29602  elspansn3  29607  normcan  29611  pjoml2  29646  lecm  29652  osum  29680  nmbdfnlb  30085  leopmul  30169  hstpyth  30264  cvnbtwn  30321  ssmd1  30346  ssmd2  30347  ssdmd1  30348  ssdmd2  30349  cvmd  30371  cvdmd  30372  superpos  30389  disji2f  30589  disjif  30590  disjif2  30593  preiman0  30716  padct  30728  ffs2  30737  bcm1n  30790  s2f1  30893  omndadd  31005  ogrpaddlt  31016  archiabl  31125  slmdlema  31129  lbslsat  31367  eulerpartlemb  32001  sgn3da  32174  fisshasheq  32740  hashfundm  32741  cvmsdisj  32899  cvmlift2lem12  32943  satfrel  32996  satfrnmapom  32999  fmlasuc  33015  satffun  33038  satef  33045  sategoelfv  33049  poseq  33482  naddssim  33523  nosepon  33554  nolesgn2o  33560  nogesgn1o  33562  nosepnelem  33568  nosepne  33569  nosepdmlem  33572  nosepdm  33573  nodenselem8  33580  noresle  33586  noetasuplem4  33625  noetainflem4  33629  scutbdaylt  33698  lineintmo  34145  nn0prpwlem  34197  nn0prpw  34198  neibastop2lem  34235  lindsadd  35456  areacirc  35556  incsequz  35592  mettrifi  35601  ismtybnd  35651  heiborlem1  35655  rngoisocnv  35825  risci  35831  eqvrelqsel  36415  lfl1  36770  lkrlsp2  36803  omlfh3N  36959  cvrnbtwn  36971  cvrnbtwn2  36975  cvrnbtwn4  36979  cvlexch3  37032  cvlexch4N  37033  cvlatexchb1  37034  2llnne2N  37108  atcvrj0  37128  cvrat2  37129  ps-1  37177  3atlem5  37187  islln2a  37217  lplnriaN  37250  lplnribN  37251  llncvrlpln2  37257  lplncvrlvol2  37315  psubatN  37455  pmapglb2N  37471  pmapglb2xN  37472  2llnma1b  37486  paddasslem17  37536  pmod2iN  37549  pmodl42N  37551  hlmod1i  37556  atmod1i1  37557  atmod1i2  37559  llnmod1i2  37560  pclcmpatN  37601  osumcllem8N  37663  pexmidlem3N  37672  pl42lem4N  37682  4atexlem7  37775  ltrnnid  37836  cdlemc4  37894  cdleme32a  38141  cdlemeg46gfre  38232  cdlemf2  38262  cdlemg4c  38312  trlcoat  38423  tendovalco  38465  tendoeq2  38474  cdlemk36  38613  diael  38743  diatrl  38744  dicelval1stN  38888  dicelval2nd  38889  dihlspsnat  39033  dochkr1  39178  lcfrlem9  39250  mapdh8e  39484  hdmapval0  39533  hgmapval0  39592  nnadddir  39948  nn0rppwr  39982  nn0expgcd  39984  dvdsexpnn0  39990  incssnn0  40177  pell14qrexpcl  40333  pell14qrgap  40341  congadd  40432  acongsym  40442  acongtr  40444  dvdsacongtr  40450  jm2.19lem3  40457  jm2.19lem4  40458  jm2.26lem3  40467  ismnushort  41533  bi13impia  41722  3impcombi  42051  ioogtlb  42649  iocgtlb  42656  iocleub  42657  icoltub  42662  iooltub  42664  limclner  42810  limsupre3lem  42891  climuzlem  42902  elfzelfzlble  44429  subsubelfzo0  44434  iccpartigtl  44491  sqrtpwpw2p  44606  fmtnoprmfac1lem  44632  fmtno4prmfac  44640  evenltle  44785  even3prm2  44787  wtgoldbnnsum4prm  44870  bgoldbnnsum3prm  44872  bgoldbtbndlem1  44873  bgoldbtbndlem3  44875  bgoldbtbndlem4  44876  bgoldbtbnd  44877  upgrwlkupwlk  44918  c0snmgmhm  45088  funcringcsetcALTV2lem9  45218  funcringcsetclem9ALTV  45241  lincscmcl  45389  lindslinindimp2lem4  45418  lincresunit2  45435  lincresunit3  45438  elfzolborelfzop1  45476  m1modmmod  45483  rege1logbzge0  45521  fllog2  45530  dignn0ldlem  45564  rrx2pnecoorneor  45677  rrx2plord2  45684  rrx2linest  45704  ipolub  45890  ipoglb  45893