Theorem 3impia 1113

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 456	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	3impib 1112	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  mopick2  2722  3gencl  3536  vtoclgft  3553  vtoclgftOLD  3554  mob2  3706  moi  3709  reupick3  4288  disjne  4404  elpr2elpr  4799  disji2  5048  disji  5049  tz7.2  5539  sofld  6044  ordintdif  6240  funopg  6389  fvun1  6754  fvopab6  6801  fveqressseq  6847  fvcofneq  6859  fprg  6917  2f1fvneq  7018  isores3  7088  ovmpt4g  7297  ovmpos  7298  ov2gf  7299  ofrval  7419  sorpssuni  7458  sorpssint  7459  poxp  7822  suppss2  7864  smoel  7997  smoord  8002  smogt  8004  oaass  8187  oewordi  8217  oeoalem  8222  oeoelem  8224  nnawordi  8247  nnaass  8248  qsel  8376  xpdom3  8615  onsdominel  8666  mapdom3  8689  fisseneq  8729  cantnflem1  9152  cfslbn  9689  cfsmolem  9692  cfcoflem  9694  infpssrlem4  9728  fin23lem7  9738  fin23lem25  9746  isf34lem7  9801  hsmexlem2  9849  axcc3  9860  axdc4lem  9877  tskss  10180  gruss  10218  gruurn  10220  gruiun  10221  gruel  10225  gruen  10234  grudomon  10239  grothac  10252  axpre-sup  10591  axsup  10716  addn0nid  11060  letrp1  11484  p1le  11485  lemul1a  11494  infrelb  11626  zextle  12056  zextlt  12057  btwnnz  12059  gtndiv  12060  uzind2  12076  fzind  12081  eluzsub  12275  zsupss  12338  xrltne  12557  lemaxle  12589  qbtwnre  12593  qbtwnxr  12594  xlemul1a  12682  icogelb  12789  iccleub  12793  iccsplit  12872  uzsubsubfz  12930  elfz0fzfz0  13013  difelfznle  13022  fvffz0  13026  elfzo0le  13082  fzonmapblen  13084  fzofzim  13085  ceile  13218  modadd1  13277  muladdmodid  13280  modmul1  13293  modirr  13311  fsuppmapnn0fiub0  13362  expcl2lem  13442  expclzlem  13454  expnegz  13464  leexp2r  13539  bcval4  13668  bccmpl  13670  hashbnd  13697  hashunsnggt  13756  hashgt23el  13786  elovmpowrd  13910  ccatval2  13932  ccatrcl1  13948  wrdl1s1  13968  ccat2s1fvw  13998  ccat2s1fvwOLD  13999  swrdsb0eq  14025  swrdccatin1  14087  pfxccatpfx2  14099  repswswrd  14146  cshwcsh2id  14190  absexpz  14665  climbdd  15028  iseraltlem2  15039  binomfallfac  15395  dvdsle  15660  divalgb  15755  ndvdssub  15760  dvdsgcd  15892  dfgcd2  15894  rplpwr  15907  lcmgcdlem  15950  lcmfunsn  15988  coprmdvds1  15996  qredeq  16001  2mulprm  16037  prmdvdsexpr  16061  nnnn0modprm0  16143  prm23ge5  16152  pcexp  16196  difsqpwdvds  16223  prmpwdvds  16240  ramcl  16365  cshwshashlem3  16431  cshwrepswhash1  16436  elrestr  16702  mreintcl  16866  mremre  16875  mrieqv2d  16910  initoeu2lem1  17274  funcestrcsetclem9  17398  funcsetcestrclem9  17413  prstr  17543  drsdirfi  17548  latnlej  17678  latnlej2  17681  acsdrsel  17777  acsdrscl  17780  mrelatglb  17794  mrelatlub  17796  isnmgm  17856  grpasscan1  18162  grpinvnz  18170  mulgneg2  18261  gsmsymgrfix  18556  f1omvdco2  18576  symggen  18598  odcl2  18692  odhash3  18701  lsmss1  18791  lsmss2  18793  efgred  18874  efgcpbl  18882  ablfacrp  19188  ablfac1eu  19195  ablfaclem3  19209  dvdsrmul1  19403  dvdsunit  19413  irredmul  19459  lmodlema  19639  ply1scln0  20459  psgnodpmr  20734  phlssphl  20803  lindsss  20968  lindfmm  20971  dmatelnd  21105  mdetdiaglem  21207  mdet0  21215  mdetunilem7  21227  slesolinv  21289  cramerimplem3  21294  cpmatpmat  21318  m2cpminvid2lem  21362  chfacfscmul0  21466  chfacfpmmul0  21470  riinopn  21516  clsndisj  21683  cnpf2  21858  hausnei2  21961  cmpcov  21997  cmpfii  22017  unconn  22037  t1connperf  22044  nrmr0reg  22357  fbfinnfr  22449  filuni  22493  alexsubALT  22659  tmdgsum  22703  cuspcvg  22910  mopni  23102  isngp4  23221  metdsre  23461  iimulcl  23541  phtpc01  23600  clmmulg  23705  cfilucfil4  23924  bcthlem5  23931  bcth  23932  bcth3  23934  itg1le  24314  itg2le  24340  bddmulibl  24439  dvnres  24528  cpnord  24532  dvnfre  24549  deg1ge  24692  dgr1term  24850  aaliou3lem2  24932  sincosq1lem  25083  cxpge0  25266  cxpmul2  25272  logrec  25341  logbgcd1irr  25372  sqfpc  25714  bcmono  25853  gausslemma2dlem1a  25941  gausslemma2dlem2  25943  gausslemma2dlem4  25945  2lgsoddprmlem3  25990  pntrmax  26140  qabvexp  26202  ostth2lem2  26210  ax5seglem4  26718  axeuclidlem  26748  uhgredgrnv  26915  usgredg4  26999  nbuhgr2vtx1edgblem  27133  vtxduhgr0e  27260  vtxduhgr0nedg  27274  rusgrpropnb  27365  uspgr2wlkeqi  27429  redwlklem  27453  lfgrwlkprop  27469  2pthnloop  27512  spthonepeq  27533  pthdlem2lem  27548  crctcshwlkn0lem3  27590  crctcshwlkn0lem5  27592  crctcshwlkn0lem7  27594  crctcshwlkn0  27599  wlkiswwlks1  27645  wlkiswwlks2  27653  wlkiswwlksupgr2  27655  wwlksnext  27671  wwlksnextproplem2  27689  wspthsnonn0vne  27696  2pthon3v  27722  rusgrnumwwlk  27754  erclwwlkeqlen  27797  erclwwlksym  27799  erclwwlktr  27800  erclwwlkneqlen  27847  erclwwlknsym  27849  erclwwlkntr  27850  uhgr3cyclex  27961  upgreupthseg  27988  eupth2lem3lem4  28010  eucrctshift  28022  4cycl2vnunb  28069  nvs  28440  nvtri  28447  nmlno0  28572  nmlnoubi  28573  ubth  28650  hlipgt0  28691  ocnel  29075  elspansn2  29344  elspansn3  29349  normcan  29353  pjoml2  29388  lecm  29394  osum  29422  nmbdfnlb  29827  leopmul  29911  hstpyth  30006  cvnbtwn  30063  ssmd1  30088  ssmd2  30089  ssdmd1  30090  ssdmd2  30091  cvmd  30113  cvdmd  30114  superpos  30131  disji2f  30327  disjif  30328  disjif2  30331  padct  30455  ffs2  30464  bcm1n  30518  s2f1  30621  omndadd  30707  ogrpaddlt  30718  archiabl  30827  slmdlema  30831  lbslsat  31014  eulerpartlemb  31626  sgn3da  31799  fisshasheq  32352  hashfundm  32354  cvmsdisj  32517  cvmlift2lem12  32561  satfrel  32614  satfrnmapom  32617  fmlasuc  32633  satffun  32656  satef  32663  sategoelfv  32667  poseq  33095  frrlem12  33134  nosepon  33172  nolesgn2o  33178  nosepnelem  33184  nosepne  33185  nosepdmlem  33187  nosepdm  33188  nodenselem8  33195  noresle  33200  noetalem3  33219  sslttr  33268  scutbdaylt  33276  lineintmo  33618  nn0prpwlem  33670  nn0prpw  33671  neibastop2lem  33708  lindsadd  34900  bddiblnc  34977  areacirc  35002  incsequz  35038  mettrifi  35047  ismtybnd  35100  heiborlem1  35104  rngoisocnv  35274  risci  35280  eqvrelqsel  35866  lfl1  36221  lkrlsp2  36254  omlfh3N  36410  cvrnbtwn  36422  cvrnbtwn2  36426  cvrnbtwn4  36430  cvlexch3  36483  cvlexch4N  36484  cvlatexchb1  36485  2llnne2N  36559  atcvrj0  36579  cvrat2  36580  ps-1  36628  3atlem5  36638  islln2a  36668  lplnriaN  36701  lplnribN  36702  llncvrlpln2  36708  lplncvrlvol2  36766  psubatN  36906  pmapglb2N  36922  pmapglb2xN  36923  2llnma1b  36937  paddasslem17  36987  pmod2iN  37000  pmodl42N  37002  hlmod1i  37007  atmod1i1  37008  atmod1i2  37010  llnmod1i2  37011  pclcmpatN  37052  osumcllem8N  37114  pexmidlem3N  37123  pl42lem4N  37133  4atexlem7  37226  ltrnnid  37287  cdlemc4  37345  cdleme32a  37592  cdlemeg46gfre  37683  cdlemf2  37713  cdlemg4c  37763  trlcoat  37874  tendovalco  37916  tendoeq2  37925  cdlemk36  38064  diael  38194  diatrl  38195  dicelval1stN  38339  dicelval2nd  38340  dihlspsnat  38484  dochkr1  38629  lcfrlem9  38701  mapdh8e  38935  hdmapval0  38984  hgmapval0  39043  nnadddir  39183  nn0rppwr  39202  nn0expgcd  39204  incssnn0  39328  pell14qrexpcl  39484  pell14qrgap  39492  congadd  39583  acongsym  39593  acongtr  39595  dvdsacongtr  39601  jm2.19lem3  39608  jm2.19lem4  39609  jm2.26lem3  39618  relexpiidm  40069  bi13impia  40842  3impcombi  41171  ioogtlb  41790  iocgtlb  41797  iocleub  41798  icoltub  41804  iooltub  41806  limclner  41952  limsupre3lem  42033  climuzlem  42044  elfzelfzlble  43541  subsubelfzo0  43546  iccpartigtl  43603  sqrtpwpw2p  43720  fmtnoprmfac1lem  43746  fmtno4prmfac  43754  evenltle  43902  even3prm2  43904  wtgoldbnnsum4prm  43987  bgoldbnnsum3prm  43989  bgoldbtbndlem1  43990  bgoldbtbndlem3  43992  bgoldbtbndlem4  43993  bgoldbtbnd  43994  upgrwlkupwlk  44035  c0snmgmhm  44205  funcringcsetcALTV2lem9  44335  funcringcsetclem9ALTV  44358  lincscmcl  44507  lindslinindimp2lem4  44536  lincresunit2  44553  lincresunit3  44556  elfzolborelfzop1  44594  m1modmmod  44601  rege1logbzge0  44639  fllog2  44648  dignn0ldlem  44682  rrx2pnecoorneor  44722  rrx2plord2  44729  rrx2linest  44749